Inference at * 
Iof proof for Lemma int lt to int upper:


  i:, A:({i + 1...}). {j:. (i < j)  A(j)}  {j:{i + 1...}. A(j)} 

latex

 by Unfold `guard` 0 

latex

 1: 

 1:   i:, A:({i + 1...}). (j:. (i < j)  A(j))  (j:{i + 1...}. A(j))
 .

Definitions

{T}